\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $i$:Id, ${\it es}$:event\_system\{i:l\}.
\\[0ex]($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; $e$); top)))
\-\\[0ex]$\Rightarrow$ \=($\forall$$e_{1}$,$e_{2}$,$e$:es{-}E(${\it es}$).\+
\\[0ex](loc($e_{2}$) = $i$)
\\[0ex]$\Rightarrow$ (loc($e_{1}$) = $i$)
\\[0ex]$\Rightarrow$ es{-}le(${\it es}$; $e$; $e_{2}$)
\\[0ex]$\Rightarrow$ iseg(event{-}info(${\it ds}$;${\it da}$); es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e$); es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$)))
\-
\end{tabbing}